
public class PointIn extends Point  {
	
	static /*@ spec_public @*/ int num_inst; 
	
	//@ invariant prox != null && prox instanceof PointOut;
	public PointOut prox;
	
	//@ requires prox != null && this != null  && n < nexts.length && this.next != null;
	PointIn(PointOut prox){
		super();
		this.prox = (PointOut) prox;//.clona();
	}
	
	//@ requires pi != null && n < nexts.length && pi.next != null ;
	PointIn(PointIn pi) {
		super(pi.next,pi.sema);
		prox=pi.prox;
		nexts[n] = pi.next.getId();
		
	}
	
	//@ requires this != null && n < nexts.length && this.next != null && this.prox != null;
	public Object clona() {
		return new PointIn(this);
	}
	

}
